($\lambda$$T$,${\it as}$,$m$,$n$,$z$. ${\it as}$[$m$..$n$$^{-}$]) $\in$ $T$:Type$\rightarrow$($T$ List)$\rightarrow\mathbb{Z}\rightarrow\mathbb{Z}\rightarrow\downarrow$True$\rightarrow$($T$ List)